#include <stdio.h>
#include <string.h>
#include <assert.h>
#include <Judy.h>

#include "../model/globals.h"
#include "../normalization/normalized_datatypes.h"
#include "../normalization/normalization_globals.h"
#include "../normalization/print_utils.h"
#include "../normalization/utils.h"
#include "../preprocessing/utils.h"
#include "utils.h"

#define IS_EMPTY_STACK  (stacks_to_process->size == 0)

// NormalizedConcept** normalized_atomic_concepts_left;
// int normalized_atomic_concepts_left_count;
Pvoid_t normalized_atomic_concepts_left;

static Pvoid_t stacks_to_process;

void init_completion() {
	int i, judy_return, judy_return1;
	Word_t index = 0;
	NormalizedConcept* c;

	stacks_to_process = (Pvoid_t) NULL;

	for (i = 0; i < normalized_atomic_concept_count ; ++i) {
		if (normalized_atomic_concepts[i]->containing_premises_count != 0) {
			c = normalized_atomic_concepts[i];
			// initially the stack and subsumer list of c contains only itself
			// push_to_concepts_to_process(c->description.atomic, c);
			push_to_axioms_to_process(c->description.atomic, c);
			add_subsumer(c->description.atomic, c);
			// now push c to stacks to process	
			J1S(judy_return, stacks_to_process, (Word_t) c->description.atomic);
			if (judy_return == JERR) {
				fprintf(stderr, "could not push to stack, aborting!\n");
				exit(-1);
			}
		}
	}
}

void process_concept_name(NormalizedAtomicConcept* ac, NormalizedConcept* c) {
	int i, judy_return1, judy_return2;
	Word_t index;
	NormalizedConcept* ex;

	// printf("--> process concept name\n");
	// printf("ac: ");
	// print_normalized_atomic_concept(ac);
	// printf("\n");
	// avoid adding an already existential restriction
	if (ac == c->description.atomic)
		return;

	for (i = 0; i < ac->number_of_filler_of; ++i) {
		index = 0;
		J1F(judy_return1, ac->filler_of[i]->subsumees, index);
		while (judy_return1 == 1) {
			ex = create_normalized_exists(ac->filler_of[i]->role, c);
			if (!is_subsumer_of((NormalizedAtomicConcept*) index, ex)) {
				push_to_axioms_to_process((NormalizedAtomicConcept*) index, ex);
				add_subsumer((NormalizedAtomicConcept*) index, ex);
			
				// now push (NormalizedAtomicConcept*) index to stack to process it again
				J1S(judy_return2, stacks_to_process, index);
				if (judy_return2 == JERR) {
					fprintf(stderr, "could not push to stack, aborting!\n");
					exit(-1);
				}

			}
			J1N(judy_return1, ac->filler_of[i]->subsumees, index);
		}
	}
}

void process_existential(NormalizedAtomicConcept* ac, NormalizedConcept* c) {
	Word_t index = 0;
	int judy_return, judy_return2;
	NormalizedConcept* ex;

	J1F(judy_return, c->description.exists->filler->description.atomic->subsumers, index); 
	while (judy_return == 1) {
		if (c->description.exists->filler != (NormalizedConcept*) index) {
			ex = create_normalized_exists(c->description.exists->role, (NormalizedConcept*) index);
			if (!is_subsumer_of(ac, ex)) {
				push_to_axioms_to_process(ac, ex);
				add_subsumer(ac, ex);

				// now push ac to stack to process it again
				J1S(judy_return2, stacks_to_process, (Word_t) ac);
				if (judy_return2 == JERR) {
					fprintf(stderr, "could not push to stack, aborting!\n");
					exit(-1);
				}
			}
		}
		J1N(judy_return, c->description.exists->filler->description.atomic->subsumers, index); 
	}
}

void process_axiom(NormalizedAtomicConcept* ac, NormalizedSubClassAxiom* ax) {
	int judy_return;
	Word_t index;

	switch (ax->rhs->type) {
		case NORMALIZED_ATOMIC_CONCEPT:
			if (!is_subsumer_of(ac, ax->rhs)) {
				push_to_axioms_to_process(ac, ax->rhs);
				add_subsumer(ac, ax->rhs);
				process_concept_name(ac, ax->rhs);
			}
			break;
		case NORMALIZED_EXISTENTIAL_RESTRICTION:
			if (!is_subsumer_of(ac, ax->rhs)) {
				push_to_axioms_to_process(ac, ax->rhs);
				add_subsumer(ac, ax->rhs);
				process_existential(ac, ax->rhs);
			}
			break;
		case NORMALIZED_CONJUNCTION:
			index = 0;
			J1F(judy_return, ax->rhs->description.conj->conjuncts, index);
			if (judy_return == 0) {
				fprintf(stderr,"no conjunct in conjunction, aborting\n");
				exit(-1);
			}
			while (judy_return == 1) {
				switch (((NormalizedConcept*) index)->type) {
					case NORMALIZED_ATOMIC_CONCEPT:
						if (!is_subsumer_of(ac, (NormalizedConcept*) index)) {
							push_to_axioms_to_process(ac, (NormalizedConcept*) index);
							add_subsumer(ac, (NormalizedConcept*) index);
							process_concept_name(ac, (NormalizedConcept*) index);
						}
            break;
					case NORMALIZED_EXISTENTIAL_RESTRICTION:
						if (!is_subsumer_of(ac, (NormalizedConcept*) index)) {
							push_to_axioms_to_process(ac, (NormalizedConcept*) index);
							add_subsumer(ac, (NormalizedConcept*) index);
							process_existential(ac, (NormalizedConcept*) index);
						}
						break;
					default:
						fprintf(stderr, "unknown normalized concept type, aborting!\n");
						exit(-1);
				}
				J1N(judy_return, ax->rhs->description.conj->conjuncts, index);
			}
			break;
		default:
			fprintf(stderr, "unknown normalized concept type, aborting!\n");
			exit(-1);
	}
}


void complete_kb() {
	NormalizedAtomicConcept* ac;
	NormalizedAxiom* ax;
	int number_of_axioms_to_process;
	int i, number_of_stacks_to_process;
	int judy_return;
	Word_t index;

	init_completion();

	J1C(number_of_stacks_to_process, stacks_to_process, 0, -1);
	while (number_of_stacks_to_process != 0) {
		index = 0;
		J1F(judy_return, stacks_to_process, index);
		if (judy_return == 0) {
			fprintf(stderr, "could not pop from stack, aborting!\n");
			exit(-1);
		}
		J1U(judy_return, stacks_to_process, index);
		ac = (NormalizedAtomicConcept*) index;

		// printf("======== concept name: %s ========\n",ac->name);
		J1C(number_of_axioms_to_process, ac->axioms_to_process, 0, -1);
		while (number_of_axioms_to_process != 0) {
			ax = pop_from_axioms_to_process(ac);
			if (subsumes(ac, ax->body.subclass_ax->lhs)) {
				process_axiom(ac, ax->body.subclass_ax);
			}
			J1C(number_of_axioms_to_process, ac->axioms_to_process, 0, -1);
		}
		J1C(number_of_stacks_to_process, stacks_to_process, 0, -1);
	}
}
